Nuprl Lemma : d-da-atom-free
0,22
postcript
pdf
D
:Dsys,
i
:Id. Feasible(
D
)
AtomFree(da(M(
i
)))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Feasible(
D
)
,
Prop
Lemmas
dsys
wf
,
Id
wf
,
d-feasible
wf
origin
D:Dsys, i:Id. Feasible(D) 
AtomFree(da(M(i))) D:Dsys, i:Id. Feasible(D) AtomFree(da(M(i))) 
T Qx:A. B(x)